the_es:ES, e:E. (isrcv(e))  sender(e) c e 

latex

Definitions	t  T, P  Q, x:A. B(x), sender(e), E, , (e < e'), P  Q, e c e', ES, isrcv(e), b
Lemmas	es-sender-causl, assert wf, es-isrcv wf, event system wf, es-E wf, es-sender wf